ABSTRACT
We present a simple yet useful technique for refining the control structure of loops that occur in imperative programs. Loops containing complex control flow are common in synchronous embedded controllers derived from modeling languages such as Lustre, Esterel, and Simulink/Stateflow. Our approach uses a set of labels to distinguish different control paths inside a given loop. The iterations of the loop are abstracted as a finite state automaton over these labels. Subsequently, we use static analysis techniques to identify infeasible iteration sequences and subtract such forbidden sequences from the initial language to obtain a refinement. In practice, the refinement of control flow sequences often simplifies the control flow patterns in the loop. We have applied the refinement technique to improve the precision of abstract interpretation in the presence of widening. Our experiments on a set of complex reactive loop benchmarks clearly show the utility of our refinement techniques. Abstraction interpretation with our refinement technique was able to verify all the properties for 10 out of the 13 benchmarks, while abstraction interpretation without refinement was able to verify only four. Other potentially useful applications include termination analysis and reverse engineering models from source code.
- Absint WCET timing analysis tool. http://www.absint.com/.Google Scholar
- Bagnara, R., Hill, P. M., Ricci, E., and Zaffanella, E. Precise widening operators for convex polyhedra. In Static Analysis Symposium (2003), vol. 2694 of LNCS, Springer, pp. 337--354. Google ScholarDigital Library
- Balakrishnan, G., Sankaranarayanan, S., Ivancic, F., Wei, O., and Gupta, A. SLR: Path-sensitive analysis through infeasible-path detection and syntactic language refinement. In SAS (2008), vol. 5079 of LNCS, pp. 238--254. Google ScholarDigital Library
- Ball, T., and Rajamani, S. K. The SLAM toolkit. In CAV (2001), vol. 2102 of LNCS, pp. 260--264. Google ScholarDigital Library
- Bardin, S., Finkel, A., Leroux, J., and Petrucci, L. FAST: Fast accelereation of symbolic transition systems. In CAV (July 2003), vol. 2725 of LNCS.Google Scholar
- Beyer, D., Henzinger, T. A., Jhala, R., and Majumdar, R. The software model checker BLAST. STTT 9, 5-6 (2007), 505--525. Google ScholarDigital Library
- Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Mine, A., Monniaux, D., and Rival, X. A static analyzer for large safety-critical software. In PLDI (June 2003), pp. 196--207. Google ScholarDigital Library
- Clarke, E., Kroening, D., and Lerda, F. A tool for checking ANSI-C programs. In TACAS (2004), vol. 2988 of LNCS.Google Scholar
- Colon, M., Sankaranarayanan, S., and Sipma, H. Linear invariant generation using non-linear constraint solving. In CAV (July 2003), vol. 2725 of LNCS, Springer, pp. 420--433.Google Scholar
- Colon, M., and Sipma, H. Synthesis of linear ranking functions. In Tools and Algorithms for Construction and Analysis of Systems (April 2001), vol. 2031 of LNCS. Google ScholarDigital Library
- Cook, B., Podelski, A., and Rybalchenko, A. Termination proofs for systems code. In PLDI (2006). Google ScholarDigital Library
- Cousot, P., and Cousot, R. Static determination of dynamic properties of programs. In Proc. ISOP'76 (1976), Dunod, Paris, France, pp. 106--130.Google Scholar
- Cousot, P., and Cousot, R. Abstract Interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In POPL (1977), pp. 238--252. Google ScholarDigital Library
- Cousot, P., and Halbwachs, N. Automatic discovery of linear restraints among the variables of a program. In POPL'78 (Jan. 1978), pp. 84--97. Google ScholarDigital Library
- Esparza, J., Hansel, D., Rossmanith, P., and Schwoon, S. Efficient algorithms for model checking pushdown systems. In CAV (2000), vol. 1855 of LNCS. Google ScholarDigital Library
- Fehnker, A., Brauer, J., Huuck, R., and Seefried, S. Goanna: Syntactic software model checking. In Auto. Tech. for Verif.&Analysis (2008). Google ScholarDigital Library
- Gaubert, S., Goubault, E., Taly, A., and Zennou, S. Static analysis by policy iteration on relational domains. In ESOP (2007), vol. 4421 of LNCS, pp. 237--252. Google ScholarDigital Library
- Gawlitza, T., and Seidl, H. Precise fixpoint computation through strategy iteration. In ESOP (2007), vol. 4421 of LNCS, pp. 300--315. Google ScholarDigital Library
- Gopan, D., and Reps, T. W. Lookahead widening. In CAV (2006), vol. 4144 of LNCS, pp. 452--466. Google ScholarDigital Library
- Gopan, D., and Reps, T. W. Guided static analysis. In SAS (2007), vol. 4634 of LNCS, pp. 349--365. Google ScholarDigital Library
- Goubault, E., and Putot, S. Static analysis of numerical algorithms. In SAS (2006), vol. 4134 of LNCS, Springer, pp. 18--34. Google ScholarDigital Library
- Gulwani, S., Jain, S., and Koskinen, E. Control-flow refinement and progress invariants for bound analysis. PLDI 2009 (to appear). Google ScholarDigital Library
- Gupta, A., Henzinger, T. A., Majumdar, R., Rybalchenko, A., and Xu, R.-G. Proving non-termination. In POPL (2008), ACM, pp. 147--158. Google ScholarDigital Library
- Halbwachs, N. Synchronous programming of reactive systems. Kluwer Academic Pub., 1993. Google ScholarDigital Library
- Halbwachs, N., Proy, Y., and Roumanoff, P. Verification of real-time systems using linear relation analysis. Formal Methods in System Design 11, 2 (1997), 157--185. Google ScholarDigital Library
- Harary, F. Graph Theory. Addison-Wesley, 1969.Google Scholar
- Ivancic, F., Yang, Z., Ganai, M. K., Gupta, A., Shlyakhter, I., and Ashar, P. F-soft: Software verification platform. In CAV (2005), vol. 3576 of LNCS. Google ScholarDigital Library
- Jeannet, B., Halbwachs, N., and Raymond, P. Dynamic partitioning in analyses of numerical properties. In Static Analysis Symposium, SAS'99 (Sep 1999), vol. 1694 of LNCS, pp. 39--50. Google ScholarDigital Library
- MathWorks Inc. Electronic vehicle climate control simulink/stateflow model. www.mathworks.com/products/simulink/demos.html.Google Scholar
- Mathworks Inc. Simulink/stateflow (tm) model-based control design environment. Cf. www.mathworks.com/simulink.Google Scholar
- Mauborgne, L., and Rival, X. Trace partitioning in abstract interpretation based static analyzers. In ESOP (2005), vol. 3444 of LNCS, pp. 5--20. Google ScholarDigital Library
- Min´e, A. A new numerical abstract domain based on difference-bound matrices. In PADO II (May 2001), vol. 2053 of LNCS, Springer, pp. 155--172. Google ScholarDigital Library
- Sankaranarayanan, S., Ivancic, F., and Gupta, A. Program analysis using symbolic ranges. In SAS (2007), vol. 4634 of LNCS, pp. 366--383. Google ScholarDigital Library
- Sankaranarayanan, S., Ivancic, F., Shlyakhter, I., and Gupta, A. Static analysis in disjunctive numerical domains. In SAS (2006), vol. 4134 of LNCS. Google ScholarDigital Library
- Simon, A., and King, A. Widening polyhedra with landmarks. In APLAS (2006), vol. 4279 of LNCS. Google ScholarDigital Library
Index Terms
- Refining the control structure of loops using static analysis
Recommendations
Pushdown control-flow analysis for free
POPL '16Traditional control-flow analysis (CFA) for higher-order languages introduces spurious connections between callers and callees, and different invocations of a function may pollute each other's return flows. Recently, three distinct approaches have been ...
Pushdown control-flow analysis for free
POPL '16: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming LanguagesTraditional control-flow analysis (CFA) for higher-order languages introduces spurious connections between callers and callees, and different invocations of a function may pollute each other's return flows. Recently, three distinct approaches have been ...
Interprocedural Pointer Analysis in Goanna
Goanna is an industrial-strength static analysis tool used in academia and industry alike to find bugs in C/C++ programs. Unlike existing approaches, Goanna uses the off-the-shelf model checker NuSMV as its core analysis engine on a syntactic flow-...
Comments